es:ES, A:Type, ds:x:Id fp Type, v:(k:Knd fp V:Type  (State(ds)V(A + Top)) List), i:Id.
((null(v)))
 (condsv. es-triggers-params-consistent(es;A;i;ds;conds))
 (conds1,conds2v.  conds1 || conds2)
 es-triggers-params-consistent(es;A;i;ds;(v)) 

latex

Definitions

x:A. B(x), t  T, x. t(x), P  Q, b, null(as), tt, if b then t else f fi , True, Top, , x,y. t(x;y), S  T, a:A fp B(a), es-triggers-params-consistent(es;A;i;ds;conds), P & Q, x:A. B(x), xL. P(x), f || g, A c B, P  Q, P  Q, x(s), A, False, x(s1,s2), Dec(P), P  Q, ff, , x  dom(f), t.1, deq-member(eq;x;L), reduce(f;k;as), Y, {T}

Lemmas

fpf wf, Knd wf, decl-state wf, top wf, Id wf, event system wf, not wf, true wf, l all cons, es-triggers-params-consistent wf, pairwise wf, fpf-compatible wf, Kind-deq wf, l all wf2, l member wf, assert wf, null wf3, es-triggers-params-join, fpf-join-list wf, pairwise-cons, decidable assert, fpf-dom wf, fpf-empty wf, es-kind wf, es-loc wf, es-E wf, fpf-empty-compatible-right, fpf-trivial-subtype-top, fpf-ap wf, fpf-join wf, fpf-compatible-join, implies functionality wrt iff